# Contributor: alpine-mips-patches <info@mobile-stream.com>
# Contributor: omni <omni+alpine@hack.org>
# Contributor: Jason Gross <jasongross9@gmail.com>
# Maintainer: alpine-mips-patches <info@mobile-stream.com>
pkgname=coq
pkgver=8.18.0
pkgrel=1
pkgdesc="Formal proof management system"
url="https://coq.inria.fr"
# riscv64: ocaml
# s390x: not useful
# 32-bit: huge package and nobody would use it there
arch="all !armhf !armv7 !x86 !s390x !riscv64"
license="LGPL-2.1-or-later"
depends="ocaml-findlib ocaml-runtime ocaml-zarith"
makedepends="
	bash
	dune
	ocaml
	ocaml-compiler-libs
	ocaml-findlib-dev
	"
options="!check" # many tests in 'make test-suite' fail
subpackages="$pkgname-doc"
source="$pkgname-$pkgver.tar.gz::https://github.com/coq/coq/archive/V$pkgver.tar.gz"

build() {
	./configure \
		-prefix /usr \
		-mandir /usr/share/man \
		-docdir /usr/share/doc \
		-libdir "$(ocamlc -where)/coq"
	make dunestrap
	dune build -p coq,coq-core,coq-stdlib
}

package() {
	dune install coq coq-core coq-stdlib \
		--prefix=/usr \
		--destdir="$pkgdir" \
		--mandir=/usr/share/man \
		--docdir=/usr/share/doc \
		--libdir="$(ocamlc -where)"
}

sha512sums="
46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50  coq-8.18.0.tar.gz
"
